/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#10=BAXM30/FONT#11=ZERO30/FONT#9=GRKL30/FONT#10=SUP/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Artificial Intelligence Laboratory, STANFORD UNIVERSITY, Stanford, California 94305

␈↓ ↓H␈↓∧Telephone 415 497-4430␈↓ 
⊗June 12, 1979 




␈↓ ↓H␈↓A. Nozaki
␈↓ ↓H␈↓ICU
␈↓ ↓H␈↓Osawa 3-10-2
␈↓ ↓H␈↓Mitaka, Tokyo
␈↓ ↓H␈↓181 JAPAN

␈↓ ↓H␈↓Dear Mr. Nozaki:

␈↓ ↓H␈↓        I␈αhave␈αread␈αand␈αagree␈αwith␈αyour␈αneat␈αproof␈αof␈αthe␈αtermination␈αof␈αthe␈αTakeuchi␈αfunction.␈α
 I
␈↓ ↓H␈↓hope to use it as an example the next time I teach about termination of recursive programs.

␈↓ ↓H␈↓        I␈α
have␈α
always␈α
supposed␈α
that␈α
this␈α
kind␈αof␈α
proof␈α
could␈α
be␈α
made␈α
conveniently␈α
by␈α
de≡ning␈αa
␈↓ ↓H␈↓rank␈α⊂function␈α⊂and␈α⊂proving␈α⊂that␈α⊂the␈α⊂referred␈α⊂cases␈α∂of␈α⊂the␈α⊂function␈α⊂are␈α⊂of␈α⊂lower␈α⊂rank.␈α⊂ In␈α∂the
␈↓ ↓H␈↓present␈α
case␈αit␈α
would␈α
seem␈αthat␈α
we␈αwould␈α
use␈α
induction␈αup␈α
to␈α␈↓	w␈↓
2␈↓␈α
and␈α
that␈αthe␈α
coe≠cient␈αof␈α
omega
␈↓ ↓H␈↓would␈αbe␈αyour␈α␈↓↓u(x,y,z)␈↓␈αand␈αthe␈αlinear␈αterm␈αwould␈αbe␈αa␈αconditional␈αexpression␈αdepending␈αon␈αyour
␈↓ ↓H␈↓case␈αanalysis.␈α We␈αwill␈αexplore␈αwhether␈αthe␈αproof␈αcan␈αbe␈αconveniently␈αexpressed␈αin␈αthat␈αway␈αand
␈↓ ↓H␈↓the␈α
role␈α
of␈α
your␈α
inner␈α
inductive␈α
proof.␈α
 Should␈α
any␈α
of␈α
us␈α
write␈α
anything␈α
about␈α
it,␈α
I'll␈α
send␈α
it␈α
to
␈↓ ↓H␈↓you.

␈↓ ↓H␈↓        The␈α∪main␈α∪interest␈α∪of␈α∪the␈α∪Takeuchi␈α∪function␈α∩for␈α∪me␈α∪is␈α∪to␈α∪be␈α∪able␈α∪to␈α∪write␈α∩computer
␈↓ ↓H␈↓checkable␈α∩proofs␈α∩of␈α∩the␈α∪properties␈α∩of␈α∩recursive␈α∩programs␈α∩in␈α∪a␈α∩neat␈α∩way,␈α∩and␈α∪the␈α∩Takeuchi
␈↓ ↓H␈↓function certainly provides a nice example.


␈↓ ↓H␈↓Sincerely,



␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Director
␈↓ ↓H␈↓Professor of Computer Science